sum_inv_orbit_eq_orbits: Summing reciprocal orbit sizes counts orbits
This lemma proves that summing 1/|orbit(x)| over every element x of X equals the number of distinct orbits. The key idea is a telescoping contribution: every orbit O of size k contains exactly k elements, each contributing 1/k to the sum, so O contributes k × (1/k) = 1 in total. Summing over all orbits gives exactly the orbit count. The proof works by reindexing the sum from elements of X to distinct orbits, then verifying each fiber sums to 1.
Interactive Lean 4 proof — click a line to see its strategy and explanation inline
Strategy: State the lemma — sum of reciprocal orbit sizes equals orbit count.
Explanation: We sum 1/|orbit(x)| over all x in the finite type X and claim the result equals |orbits A|, the number of distinct orbits. We work in ℚ so that division is well-defined. The intuition: each orbit of size k has k elements each contributing 1/k, totalling 1 per orbit. This lemma is a key ingredient in the proof of Burnside's Lemma.
Strategy: Introduce the key auxiliary equality h_orbit_sum.
Explanation: We claim the sum over all elements x equals a sum of 1's indexed by distinct orbits. The right-hand side uses Finset.image (fun x => orbit A x) Finset.univ, which is the finset of all distinct orbits (each orbit appears exactly once). Once proved, the RHS is simply the count of distinct orbits, giving us what we need. This have isolates the combinatorial core of the argument.
Strategy: Reindex the sum from elements to orbits using Finset.sum_image'.
Explanation: Finset.sum_image' rewrites a sum ∑ x, f(φ(x)) into ∑ o ∈ image(φ), ∑ x in fiber(o), f(o). Here φ = orbit A, so it groups elements of X by their orbit. After the rewrite, we must prove: for each orbit representative x, the sum of 1/|orbit(y)| over all y with orbit(y) = orbit(x) equals 1. The intro x hx fixes an arbitrary orbit representative x ∈ Finset.univ.
Strategy: Relate the abstract orbit cardinality to a concrete filter count.
Explanation: Fintype.card (orbit A x) is the abstract cardinality of the orbit as a subtype of X. We need to connect this to the concrete finset count of elements y ∈ X whose orbit equals orbit(x). These are equal because orbits partition X: y ∈ orbit(x) if and only if orbit(y) = orbit(x) (orbits are either identical or disjoint). This equality is what allows us to cancel the orbit size against the 1/|orbit| terms.
Strategy: Convert subtype cardinality to filter cardinality, then prove membership iff.
Explanation: Fintype.card_of_subtype rewrites Fintype.card {y | P y} as Finset.card (Finset.filter P Finset.univ), provided we prove the membership criterion matches. After the rewrite, the goal becomes: for all y, y ∈ filter (orbit A y = orbit A x) univ ↔ y ∈ orbit A x. The simp only unfolds the orbit definition and simplifies the filter membership. We then split into two directions with constructor.
Strategy: Forward direction — orbit equality implies membership.
Explanation: Assume h : orbit A y = orbit A x. We must show y ∈ orbit A x. Since y ∈ orbit A y (witnessed by the identity: A.act 1 y = y by A.one_act), and orbit A y = orbit A x by hypothesis h, we get y ∈ orbit A x via h.subset. The witness ⟨1, by simp [A.one_act]⟩ provides the proof that y ∈ orbit A y.
Strategy: Backward direction — membership implies orbit equality, proved by set extensionality.
Explanation: Assume y ∈ orbit A x, i.e., ∃ g, A.act g x = y. The rintro ⟨g, rfl⟩ destructs this, substituting y := A.act g x. We must show orbit A (A.act g x) = orbit A x as sets. Using ext, this reduces to: for all z, z ∈ orbit(g·x) ↔ z ∈ orbit(x). Forward (z = A.act h (A.act g x)): by A.mul_act, z = A.act (h*g) x ∈ orbit(x). Backward (z = A.act h x): z = A.act (h*g⁻¹) (A.act g x) ∈ orbit(g·x), using A.mul_act and simp to cancel g⁻¹·g = 1.
Strategy: Normalize orbit sizes inside the fiber sum — replace orbit(y) with orbit(x).
Explanation: Inside the fiber sum (over all y with orbit(y) = orbit(x)), every term is 1/|orbit(y)|. Since the filter hypothesis hy gives orbit(y) = orbit(x), we can replace orbit(y) with orbit(x) everywhere. Finset.sum_congr rfl applies a pointwise rewrite to each term in the sum without changing the index set. After this rewrite, every term in the fiber sum is the same constant 1/|orbit(x)|, so the sum becomes |fiber| × (1/|orbit(x)|).
Strategy: Close the fiber sum goal automatically.
Explanation: After the sum_congr rewrite, the goal is: (Finset.card (filter (orbit A · = orbit A x) univ) : ℚ) * (1 / |orbit A x|) = 1. Combined with h_card, which equates the filter card with Fintype.card (orbit A x), this reduces to k * (1/k) = 1 for k = |orbit A x|. aesop handles this arithmetic identity automatically, including the non-zero condition on k (orbits are non-empty since x ∈ orbit(x) via the identity action).
Strategy: Apply h_orbit_sum and simplify the RHS to the orbit count.
Explanation: convert h_orbit_sum using 1 applies our auxiliary lemma, leaving two sub-goals for the two sides. The simp only then simplifies the RHS: Finset.sum_const rewrites a sum of a constant 1 over a finset of size n as n • 1; nsmul_eq_mul converts n • (1:ℚ) to n * 1; mul_one simplifies to n; and Fintype.card_ofFinset converts the finset card to a Fintype card. The result is that the RHS becomes Fintype.card (orbits A), matching the goal.
Strategy: Convert the abstract orbit count to a concrete finset cardinality.
Explanation: orbits A is defined as the subtype { o | ∃ x, o = orbit A x }. Fintype.card_of_subtype rewrites its abstract cardinality as the cardinality of the finset of all sets o satisfying ∃ x, o = orbit A x. This leaves the goal: for all o, o ∈ Finset.image (orbit A) Finset.univ ↔ ∃ x, o = orbit A x, which is exactly the definition of membership in the image finset.
Strategy: Close the final membership iff goal automatically.
Explanation: The remaining goal is: ∀ o, o ∈ Finset.image (fun x => orbit A x) Finset.univ ↔ ∃ x, o = orbit A x. aesop unfolds Finset.mem_image and Finset.mem_univ, then matches the existential witnesses on both sides. Forward: if o = orbit A x for some x ∈ univ, then ∃ x, o = orbit A x. Backward: if ∃ x, o = orbit A x, then x ∈ univ (trivially) and o = orbit A x, so o ∈ image. This is a straightforward logical equivalence that aesop closes automatically. □
💡 Tip: Click on any line above to see its strategy and explanation inline. Click again to hide it.
The proof follows a clean reindexing argument:
Key insight: Orbits partition X, so every element belongs to exactly one orbit. An orbit of size k contributes k terms of 1/k each, totalling 1. Summing over all elements of X is therefore the same as summing 1 over all distinct orbits, which is exactly the orbit count.
Rewrites ∑ x, f(φ(x)) as ∑ o ∈ image(φ), ∑ x in fiber(o), f(o). Here φ = orbit A, grouping elements of X by their orbit so the outer sum runs over distinct orbits. This is the core reindexing step of the proof.
Converts an abstract subtype cardinality Fintype.card {y | P y} into a concrete finset cardinality Finset.card (Finset.filter P Finset.univ), provided the membership criterion is verified. Used twice: once for orbit cardinality, once for the orbits count.
Applies a pointwise rewrite to each term in a finset sum without changing the index set. Used to replace orbit(y) with orbit(x) inside the fiber sum, making all terms identical so the sum collapses to |fiber| × (1/|orbit(x)|).
Finset.sum_const rewrites a sum of a constant c over a finset of size n as n • c. Combined with nsmul_eq_mul (n • c = n * c) and mul_one, this simplifies the sum of 1's over the distinct orbits finset to the orbit count as a rational number.
This lemma is the orbit-counting heart of Burnside's Lemma. It formalises the classical observation that orbits partition the set X, and that summing 1/|O| over all elements of an orbit O gives exactly 1. In the Burnside proof, it is invoked to convert ∑ₓ |Stab(x)| = ∑ₓ |G|/|orbit(x)| = |G| · ∑ₓ 1/|orbit(x)| into |G| · |orbits|, completing the double-counting argument. The proof technique — reindexing a sum over a set by the image of a map — is a standard and reusable pattern in combinatorial formalisation in Lean 4.